\chapter{Bases FLWA}
\section{Introducción}
Para llevar a cabo este proyecto y poder dar origen a la construcción de \emph{FLWA} fue necesario el uso de algunos componentes o elementos que fueron vitales al momento de realizar determinada tarea. \emph{FLWA} logra conectarse con otras herramientas de manera de proporcionar ciertos resultados en conjunto.\\
\emph{FLWA} trabaja como intermediario entre otras tecnologías existentes, toma como requisito un modelo creado mediante la herramienta \emph{YAWL} para ser interpretado luego y por medio de interacción gráfica, \emph{FLWA}brindará la posibilidad de crear fluentes y propiedades. Posteriormente el modelo es traducido a \emph{FSP} por medio de la herramienta \emph{yawl2fsp} y las propiedades y fluentes son expresadas usando la lógica \emph{FLTL}(\textit{Fluent Linear Temporal Logic}) la cual, dará flexibilidad al describir escenarios complejos de comportamiento. \emph{LTSA}, por su parte, verificará las propiedades bajo el proceso especificado y finalmente \emph{FLWA} visualizará los resultados de éstas.\\\newline
Es por esto que en este capítulo tendrá como principal objetivo describir todos los componentes que dieron origen o que participaron en la construcción de la herramienta \textit{FLWA}. Se describirá el rol importante que tuvo \textit{YAWL}, posteriormente \textit{yawl2fsp} y por último \textit{LTSA}. Por otra parte, presentaremos a DECLARE una herramienta que permite analizar restricciones sobre modelos declarativos, el objetivo es mostrar el origen de una serie de plantillas de propiedades usualmente analizadas, pero que, a diferencia de DECLARE, en nuestro caso pueden ser verificadas sobre modelos procedurales de workflows. Con el fin de aportar una visión integradora, en cada ocasión se detallarán aspectos técnicos de la comunicación entre \emph{FLWA} y la correspondiente herramienta utilizada.

\section{YAWL}
Como se mencionó en el capítulo anterior, \emph{YAWL} permite definir modelos de negocio mediante un potente editor gráfico. Estos modelos serán los que este proyecto se centrará y serán objeto para realizar todo el estudio necesario para la aplicación de propiedades, las cuales serán verificadas posteriormente mediante la herramienta \textit{LTSA}.\\
Al igual que numerosas herramientas existentes, \emph{YAWL} almacena toda la información de cada componente, tanto gráfica como lógica, en diferentes archivos. Estos archivos pueden ser ``leídos'' para capturar toda esta información y luego procesarla de manera que sea posible definir sobre los modelos las propiedades que se pretenden analizar de los mismos.

Los archivos generados por la herramienta \textbf{YAWL}, como se describió anteriormente son realizados en lenguaje \textit{XML}, donde cada etiqueta que éste posee contiene información de los diferentes elementos del modelo representado. Algunas de estas etiquetas serán visualizadas y detalladas a continuación y luego en el capítulo 5 se analizarán con un enfoque mas técnico.

\lstset{
	frame=tlrb,
	language=xml,
	showstringspaces=false,
	keywordstyle=\color{blue}, morekeywords={decomposition,task,id,flowsInto,name,join,split,container,points,vertex,label,decorator,source,target,flow},
	tabsize=2, 
}

\begin{lstlisting}
<decomposition id="ReportFault"></decomposition>
<task id="Calculate_Time_Out">
	<name>Calculate Time Out</name>
	<flowsInto>
		<nextElementRef id="unnamed_6" />
	</flowsInto>
	<join code="xor" />
	<split code="and" />
</task>
<container id="Calculate_Time_Out">
	<vertex>
		<attributes>...</attributes>
	</vertex>
	<label>
		<attributes>...</attributes>
	</label>
	<decorator type="AND_split">
		<attributes>...</attributes>
	</decorator>
</container>
<flow source="Modify_Pickup_Apm" target="unnamed_11">
    <attributes>...</attributes>
</flow>
\end{lstlisting}

Éste es un ejemplo de como está formado un modelo creado por \emph{YAWL} o que es lo que contiene en su interior. Esta información será procesada para la interpretación gráfica del modelo. A continuación se detalla solo algunos de las etiquetas mas importantes que lo conforman. En el capítulo 5 se detallarán el restante de las etiquetas y que información técnica se puede extraer de ellas.

\begin{table}[tph]
        \centering
	\begin{tabular}{| p{3cm} | p{11cm} |}
		\hline
		\multirow{3}{2cm}{\centering \textit{<<decomposition>>}}	& Para esta etiqueta se le puede extraer la información a las diferentes sub-redes definidas en el modelo en el caso de que éste las contenga.\\
		\hline
	\end{tabular}
	\centering
	\begin{tabular}{| p{3cm} | p{11cm} |}
		\hline
		\multirow{6}{2cm}{\centering \textit{<<task>>}}	& Esta etiqueta representa la información sobre una tarea especifica. Comprende el nombre de la miasma, el identificador. Por otra parte contiene los identificadores de las tarea o condiciones con los que se relacione. También incluye información gráfica.\\
		\hline
	\end{tabular}
        \centering
	\begin{tabular}{| p{3cm} | p{11cm} |}
		\hline
		\multirow{6}{2cm}{\centering \textit{<<container>>}}	& Para el caso de esta etiqueta, se centra la información para las tareas y condiciones que no han sido declaradas como especificas, es decir que pueden representar a una tarea o una condición auxiliar. Además contiene la información gráficas de éstas y de las compuertas si ésta presentara.\\
		\hline
	\end{tabular}
\end{table}
\begin{table}[tph]	
	\centering
	\begin{tabular}{| p{3cm} | p{11cm} |}
		\hline
		\multirow{6}{2cm}{\centering \textit{<<flow>>}}	& Es la etiqueta que contiene los datos de las relaciones entre elementos, es decir las relaciones que se pueden presentar entre las condiciones y las tareas. Como las anteriores tiene información referida a las flechas que representa la relación y los puntos de origen y destino de la misma.\\
		\hline
	\end{tabular}
\end{table}

A continuación se introducirá una herramienta que facilitara la traducción de estos modelos a la lógica elegida \emph{FSP}, se describirán las formas en que se realizan las traducciones de algunos de los elementos de los modelos con los resultados correspondientes.

\section{YAWL2FSP}
A lo largo de los capítulos se mencionó una herramienta muy importante creado en el marco de este proyecto con el objetivo de realizar la traducción de los modelos de \textit{YAWL} a un formalismo que permita su análisis formal. \textit{YAWL2FSP}, como lo indica su nombre, toma como entrada modelos de workflows especificados en el lenguaje \emph{YAWL} (archivos con formato XML y extensión .yawl) y produce como salida un archivo que contiene una especificación \emph{FSP} que describe el comportamiento abstracto del workflow.\\
Por otro lado esta herramienta se ejecuta directamente desde linea de comando indicándole, entre otros parámetros que analizaremos en detalle en el capítulo 5, el archivo del modelo yawl a traducir. A continuación se puede ver la traducción de algunos elementos realizados por \emph{yawl2fsp}\cite{Ricci2012}.\newline

Las tareas y las condiciones se modelan en \textit{FSP} como procesos simples que tienen un evento de comienzo y uno de fin. Éstos están forzados a ocurrir en ese orden y de manera cíclica, como es natural. Para cada tarea atómica $t \in T_A$ (siendo $T_A$ el conjunto de tareas del modelo) se genera una instancia del siguiente proceso: 

\begin{shaded}
$$TASK = (start ->end -> TASK)$$
\end{shaded}

También las compuertas de las tareas se definen como procesos simples. La traducción a \textit{FSP} es la siguiente.


\begin{shaded}
\begin{align*}
XOR\_J&OIN(N=2) = (\\
	&  in[1..N] -> JOINING\\
	&|\>\>o\_cond -> XOR\_JOIN\\
),\tab\\
JOINI&NG = (\\
	&  out -> XOR\_JOIN\\
	&|\>\> o\_cond -> XOR\_JOIN\\
)\tab
\end{align*}
\end{shaded}


Para entender mejor el funcionamiento de \textit{yawl2fsp} se procederá a tomar como ejemplo el modelo que utilizamos en la sección anterior\textit{SimpleMakeTripProcess.yawl}, cuyo código será presentado a continuación pero con varias secciones omitidas para facilitar lectura. Sin embargo, \emph{yawl2fsp} omite todos los detalles gráficos que el archivo del modelo contiene.

\begin{shaded}
\lstset{language=xml, breaklines=true, basicstyle=\footnotesize\ttfamily}
\lstinputlisting{codes/codeYawl.xml}
\end{shaded}

El resultado de ejecutar \textit{SimpleMakeTripProcess.yawl} con \textit{yawl2fps} es un archivo de extensión \textit{.lts} conteniendo la traducción de ese modelo en el lenguaje FPS. El contenido del archivo traducido puede separarse en tres partes, i) un preámbulo inicial, donde se encuentran especificados los procesos correspondientes a cada tipo de elemento del lenguaje \emph{YAWL} (tareas, condiciones, gates, etc.), ii) la instanciación para cada elemento del modelo con su correspondiente proceso, y iii) la composición de estas instancias capturando el comportamiento del sistema en su totalidad.\\
A continuación sólo mostraremos un segmento inicial del preámbulo donde puede observarse el código correspondiente a la caracterización de las tareas, condiciones y compuertas OR\_JOIN y OR\_SPLIT. 

\begin{shaded}
\lstset{language=xml, breaklines=true, basicstyle=\footnotesize\ttfamily}
\lstinputlisting{codes/codeFPS.lts}
\end{shaded}

Con esta caracterización abstracta del workflow, podemos utilizar herramientas automáticas, como la que presentaremos en 3.4 para su análisis.\\

\subsection{FLWA - yawl2fsp}
Como se ha mencionado a lo largo de esta sección, \emph{FLWA} hace uso de la herramienta \emph{yawl2fps} para obtener la traducción completa del modelo \emph{YAWL}, para poder completar este proceso \emph{FLWA} toma la descripción de dicho modelo y la transfiere directamente a \emph{yawl2fps}. Una vez obtenido el modelo traducido, \emph{FLWA} incorpora al mismo la especificación de todas las propiedades sobre dicho modelo a verificar (incluyendo la definición de los fluentes presentes en las mismas).\\
\newline
Mas adelante se detallará todo el proceso de traducción de las propiedades y fluentes de una representación a otra, y que rol cumple \emph{yawl2fsp} en este proceso. También se explicará la comunicación entre \emph{FLWA} y \emph{yawl2fps} con mayor detalle en el capítulo 5.

\section{LTSA}
\emph{LTSA} o \textit{Labelled Transition System Analyser} es una herramienta para la verificación de sistemas concurrentes. De manera automática, \emph{LTSA} permite el análisis de sus modelos mediante la verificación de propiedades que especifican ciertos comportamientos del mismo. Por otra parte, \emph{LTSA} facilita la animación de trazas de ejecución del modelo, permitiendo visualizar el comportamiento del sistema de manera interactiva.\\\newline
Un sistema en \emph{LTSA} es modelado como un conjunto de maquinas finita de estado que interactúan entre sí, como se describió en la sección 2.5(\emph{FSP}). \emph{LTSA} realiza un análisis de alcanzabilidad composicional para buscar exhaustivamente violaciones a las propiedades definidas sobre los procesos. Formalmente, cada componente de una especificación es descripta como un sistema de transición de estados \textit{LTS}, la cual contiene todos los estados de un componente que pueden ser alcanzados y además todas las transiciones que puede realizar dicha especificación. Sin embargo, la descripción explícita de un LTS en términos de sus estados, el conjunto acciones, etiquetas y transiciones, se torna impracticable para sistemas que no son pequeños en los que a complejidad se refiere.\\\newline
Como consecuencia a este inconveniente, \emph{LTSA} soporta una notación basada en álgebras de procesos (\textit{FSP}) que permite, de manera compacta, dar una descripción exacta del comportamiento de los componentes. Además, como detallaremos más adelante, \emph{LTSA} cuenta entre sus funcionalidades con la posibilidad de visualizar de manera gráfica los LTSs correspondientes a cada componente o al sistema en general.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.7]{images/ltsaToolFSP.png}
\caption{\emph{LTSA} usando \emph{FSP} como especificación de un Proceso }
\end{figure}

En la figura 3.2 muestra la pantalla principal de \emph{LTSA}. La misma presenta un menú de funcionalidades como la compilación y verificación de la especificación y un editor que permite editar el código \textit{FSP} del modelo. Mediante un proceso de compilación y análisis obtendríamos posteriormente lo que se muestra la figura 3.3. En ella se puede ver el correspondiente \textit{LTS} (Sistema de transición de estados) del modelo de la figura 3.2.\\
\newline
\emph{LTSA} tiene la opción de usar un simulador permitiendo así ver de alguna manera distintos escenarios que puedan ocurrir en la ejecución de un proceso de negocio. Otras posibilidades que brinda esta herramienta es la de minimizar estados, comprobar si el modelo especificado presenta \textit{deadlock}\footnote{Deadlock: es el bloqueo permanente de un conjunto de procesos o hilos de ejecución en un sistema concurrente que compiten por recursos.} o incluso la verificación de propiedades. Esta última característica va tomar protagonismo en este trabajo ya que es la encargada de validar las propiedades que pueda presentar los modelos que tratemos en \emph{FLWA}.

\begin{figure}[h!]
\centering
\includegraphics[scale=0.8]{images/ltsaToolLTS.png}
\caption{Ejemplo de representación gráfica de un \textit{LTS} generado a partir de una especificación \textit{FSP}.}
\end{figure}

\subsection{FLWA - LTSA}
Al igual que ocurre con la comunicación con \textit{yawl2fsp}, \textit{FLWA} recurre al mismo camino incluyendo sólo la parte lógica de la plataforma \textit{LTSA}. Esto es debido a que \emph{LTSA} posee interfaz gráfica y FLWA no hace uso de esta característica. Por otra parte, \emph{FLWA} utiliza los servicios brindados por \emph{LTSA} para controlar la verificación y el análisis de los resultados que genera la misma.\\


\newpage
\section{DECLARE}
\emph{DECLARE} es una herramienta que provee un ambiente para la verificación de propiedades sobre modelos declarativos. Esto es, dada una descripción de tareas y dependencias entre las mismas, DECLARE permite analizar si dicha especificación las satisface ciertas propiedades.\\\newline

Nuestro interés sobre esta herramienta es que la misma provee un conjunto de de propiedades que usualmente forman parte del análisis de modelos declarativos, y que en nuestro caso, brindamos la posibilidad de verificarlas sobre modelos procedurales de workflows. De la misma manera en que \emph{YAWL} soporta patrones de workflow, DECLARE apunta a soportar un conjunto de plantillas que capturen algunas de las propiedades más utilizadas durante el modelado. La semántica de estas plantillas está dada en términos de fórmulas \emph{LTL}.  A continuación detallamos algunas de las plantillas que fueron tomadas de la herramienta y que pueden instanciarce dentro de \emph{FLWA} para su análisis de modelos de \emph{YAWL}.\\\newline

Un ejemplo de una plantilla tomada de \emph{DECLARE} que se puede aplicada a \emph{FLWA} es la llamada ``elección 1 de 3''. Como muestra en la figura 3.4, esta plantilla expresa que de las tres actividades elegidas dentro de ésta al menos una debe ser ejecutada. 

\begin{figure}[h!]
\centering
\includegraphics[scale=0.5]{images/exampleTemplate.png}
\caption{Ejemplo de la plantilla \textit{``choise 1 of 3''}}
\end{figure}